Step of Proof: my_tidentity_wf
12,41
postcript
pdf
Inference at
*
I
of proof for Lemma
my
tidentity
wf
:
A
:Type. Id{
A
}
A
A
latex
by Unfold `tidentity` 0
latex
1
:
1:
A
:Type. Id
A
A
.
Definitions
Id{
T
}
origin
A:Type. Id{A} 
A
A
by Unfold `tidentity` 0
1:
1: A:Type. Id AA
. A:Type. Id{A} AA
by Unfold `tidentity` 0
1:
1: A:Type. Id AA
.